(set-logic QF_BV)
(declare-fun x0 () (_ BitVec 32))
(declare-fun x1 () (_ BitVec 32))
(declare-fun x2 () (_ BitVec 32))
(declare-fun x3 () (_ BitVec 32))
(declare-fun x4 () (_ BitVec 32))
(assert (let ((?v_18 (bvadd x0 x1))) (let ((?v_22 (bvadd ?v_18 x3))) (let ((?v_23 (bvsub (_ bv0 32) ?v_22))) (let ((?v_13 (bvadd (_ bv0 32) x4))) (let ((?v_16 (bvadd ?v_13 x2))) (let ((?v_21 (bvadd ?v_16 (_ bv0 32)))) (and true (bvult ?v_23 (_ bv46 32)) true (bvult x2 (_ bv256 32)) true (bvule x4 x2) true (= (_ bv38 32) x1) true (= (_ bv104 32) x3) true (= ?v_21 x0) true))))))))
(check-sat)
(exit)
